Step of Proof: append_overlapping_sublists 11,40
Inference at * 1 2 2 2 
Iof proof for Lemma append overlapping sublists:



1. T : Type
2. L1 : T List
3. L2 : T List
4. L : T List
5. x : T
6. i, j:. (i < ||L||)  (j < ||L||)  ((i = j))  ((L[i] = L[j]))
7. f1 : {0..||L1 @ [x]||}{0..||L||}
8. increasing(f1;||L1 @ [x]||)
9. j:{0..||L1 @ [x]||}. (L1 @ [x])[j] = L[(f1(j))]
10. f : {0..(||L2||+1)}{0..||L||}
11. increasing(f;||L2||+1)
12. j:{0..(||L2||+1)}. [x / L2][j] = L[(f(j))]
13. ||L1 @ [x / L2]|| = ||L1||+||L2||+1
14. ||[]||  0 
15. j : {0..||L1 @ [x / L2]||}
  (L1 @ [x / L2])[j] = L[if j z ||L1|| then f1(j) else f(j - ||L1||) fi ] 
latex
 by InteriorProof ((((AssertBY ||L1 @ [x]|| = ||L1||+1  
 by ((((RWO "length_append" 0) 

 by ((((RWO "lengthCollapseTHEN (Reduce 0))) 
CollapseTHEN ((Auto_aux (first_nat 1:n
CollapseTHEN ((Aut) ((first_nat 1:n),(first_nat 3:n)) (first_tok SupInf:t) inil_term)))) 

CollapseTHEN ((Aut)CollapseTHEN (SplitOnConclITE))) 
CollapseTHENA ((Auto_aux (first_nat 1:n
CollapseTHENA ((Au) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term))) 
latex

C1: .....truecase..... NILNIL

C1: 16. ||L1 @ [x]|| = ||L1||+1
C1: 17. j  ||L1||
C1:   (L1 @ [x / L2])[j] = L[(f1(j))]
C2: .....falsecase..... NILNIL

C2: 16. ||L1 @ [x]|| = ||L1||+1
C2: 17. ||L1|| < j
C2:   (L1 @ [x / L2])[j] = L[(f(j - ||L1||))]
C.

DefinitionsY, ||as||, T, ff, P  Q, P & Q, P  Q, tt, if b then t else f fi , P  Q, x:A. B(x), True, , t  T, Unit, , {i..j},
Lemmaslength append, assert of lt int, bnot of le int, true wf, squash wf, eqff to assert, assert of le int, eqtt to assert, iff transitivity, bnot wf, lt int wf, le wf, assert wf, bool wf, length wf1, le int wf

origin